p:FinProbSpace, n:, X, Y:RandomVariable(p;n). rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;Y;X) 

latex

Definitions	t  T, x:A. B(x), Outcome, x:AB(x), S  T, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , , {i..j}, RandomVariable(p;n), , #$n, Type, suptype(S; T), f(a), s = t, , P  Q, {T}, left + right, rv-disjoint(p;n;X;Y), FinProbSpace
Lemmas	rv-disjoint wf, random-variable wf, nat wf, finite-prob-space wf, not wf, rationals wf, int seg wf, p-outcome wf